es-p-le-pred(es;P)(e,e')
== e' loc e  & P(e') & (e'':E. e'' loc e   (e' <loc e'')  ((P(e'')))) 

latex

---

clarification:

es-p-le-pred(es;P)(e,e')
== es-le(es;e';e)
== & P(e')
== & (e'':es-E(es). es-le(es;e'';e)  es-locl(es; e'; e'')  ((P(e'')))) 

latex

Definitions	x.A(x), P & Q, x:A. B(x), E, e loc e' , P  Q, (e <loc e'), A, f(a)
FDL editor aliases	es-p-le-pred